Nuprl Lemma : ma-single-effect0_wf2
0,22
postcript
pdf
A
,
T
:Type,
x
:Id,
a
:Knd,
f
:(
A
T
A
). ma-single-effect0(
x
;
A
;
a
;
T
;
f
)
MsgA
latex
Definitions
ma-single-effect0(
x
;
A
;
k
;
T
;
f
)
,
x
:
A
.
B
(
x
)
,
Knd
,
Id
,
t
T
Lemmas
Id
wf
,
Knd
wf
,
ma-single-effect0
wf
origin
A, T:Type, x:Id, a:Knd, f:(A
TA). ma-single-effect0(x;A;a;T;f) 
MsgA A, T:Type, x:Id, a:Knd, f:(ATA). ma-single-effect0(x;A;a;T;f) MsgA x:A. B(x) T